(set-logic QF_BV)
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ BitVec 32))
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert 
(let ((?x4 (_ bv1 32))) 
(let (($x9 (= y (_ bv0 32)))) 
(let (($x13 $x9)) 
(let (($x14 (distinct x (_ bv0 32)))) 
(let (($x17 (not $x13))) 
(let (($x18 $x17)) 
(let (($x19 (and $x9 $x14))) 
(let (($x21 $x19)) 
(let (($x22 (and $x21 $x14))) 
(let (($x26 (and $x22 $x9))) 
(let (($x27 $x21)) 
(let (($x28 (or $x26 $x27))) 
(let ((?x30 (ite $x26 ?x4 (_ bv0 32)))) 
(let ((?x38 (ite $x28 (_ bv0 32) ?x4))) 
(let ((?x39 (ite $x28 ?x30 ?x4))) 
(let ((?x42 ?x38)) 
(let ((?x43 (ite $x18 (_ bv0 32) ?x39))) 
(let (($x62 (= ?x43 ?x42))) 
(let (($x63 (and a $x62))) 
(let (($x69 (not $x63))) 
(let (($x70 $x69)) 
(let (($x71 (not $x70))) 
(let (($x72 (or b $x71))) 
(let (($x87 $x72)) $x87)))))))))))))))))))))))))
(check-sat)
(exit)
